*****************************************************
A Hilbert style axiomisation of propositional calculus derived
from Mendelson 'Introduction to Mathematical Logic'.  Implication
and negation are primitive.

(define system-L
 {--> symbol}
 -> (kb-> 

      (protect [[prv [imp P [imp Q P]]]
      [prv [imp [imp P [imp Q R]] [imp [imp P Q] [imp P R]]]]
      [prv [imp [imp [neg P] [neg Q]] [imp [imp [neg P] Q] P]]]
      [[[prv [imp P Q]] & [prv P]] => [prv Q]]
      
      [[prv [or P Q]] <=> [prv [imp [neg P] Q]]]
      [[prv [and P Q]] <=> [prv [neg [or [neg P] [neg Q]]]]]
      [[prv [equiv P Q]] <=> [prv [and [imp P Q] [imp Q P]]]]])))
      
(system-L)

(<-kb [prv [or p [neg p]]])

run time: 0.0 secs
816 inferences, equality = false
depth = 8, complexity = -1, timeout = 60 secs
true
*****************************************************
Step 1

? (prv (or p (neg p)))


> revsk
=============================
Step 2

? (prv (or p (neg p)))


> hypdisj
=============================
Step 3

? (prv (or p (neg p)))


> ((prv (or X Y)) <-- (prv (imp (neg X) Y)))
=============================
Step 4

? (prv (imp (neg p) (neg p)))


> ((prv X) <-- (prv (imp Y X)) (prv Y))
|=============================
|Step 5
|
|? (prv (imp Var42 (imp (neg p) (neg p))))
|
|
|> ((prv X) <-- (prv (imp Y X)) (prv Y))
||=============================
||Step 6
||
||? (prv (imp (imp (neg p) (imp Var52 (neg p))) (imp (imp (neg p) Var52) (imp (neg p) (neg p)))))
||
||
||> ((prv (imp (imp Y (imp X Z)) (imp (imp Y X) (imp Y Z)))) <--)
|=============================
|Step 7
|
|? (prv (imp (neg p) (imp Var52 (neg p))))
|
|
|> ((prv (imp Y (imp X Y))) <--)
=============================
Step 8

? (prv (imp (neg p) (imp Var57 (neg p))))


> ((prv (imp Y (imp X Y))) <--)
